Issue3289.agda:15,6-8
Cannot eliminate type R with projection pattern ⦃ .x ⦄
when checking that the clause f₂ ⦃ .x ⦄ = 0 has type R
